Computing Tiny Clause Normal Forms
Identifieur interne : 001176 ( Main/Exploration ); précédent : 001175; suivant : 001177Computing Tiny Clause Normal Forms
Auteurs : Noran Azmy [Allemagne] ; Christoph Weidenbach [Allemagne]Source :
Abstract
Automated reasoning systems which build on resolution or superposition typically operate on formulas in clause normal form (CNF). It is well-known that standard CNF translation of a first-order formula may result in an exponential number of clauses. In order to prevent this effect, renaming techniques have been introduced that replace subformulas by atoms over fresh predicates and introduce definitions accordingly. This paper presents generalized renaming. Given a formula and a set of subformulas to be renamed, it is suggested to use one atom to replace all instances of a generalization of a given subformula. A generalized renaming algorithm and an implementation as part of the SPASS theorem prover are described. The new renaming algorithm is faster than the previous one implemented in SPASS. Experiments on the TPTP show that generalized renaming significantly reduces the number of clauses and the average time taken to solve the problems afterward.
Url:
DOI: 10.1007/978-3-642-38574-2_7
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 001783
- to stream Hal, to step Curation: 001783
- to stream Hal, to step Checkpoint: 001093
- to stream Main, to step Merge: 001187
- to stream Main, to step Curation: 001176
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Computing Tiny Clause Normal Forms</title><author><name sortKey="Azmy, Noran" sort="Azmy, Noran" uniqKey="Azmy N" first="Noran" last="Azmy">Noran Azmy</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-397675" status="INCOMING"><orgName>Automation of Logic</orgName><desc><address><country key="DE"></country></address></desc><listRelation><relation active="#struct-54489" type="direct"></relation><relation active="#struct-300044" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-54489" type="direct"><org type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300044" type="indirect"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00931893</idno><idno type="halId">hal-00931893</idno><idno type="halUri">https://hal.inria.fr/hal-00931893</idno><idno type="url">https://hal.inria.fr/hal-00931893</idno><idno type="doi">10.1007/978-3-642-38574-2_7</idno><date when="2013-06-09">2013-06-09</date><idno type="wicri:Area/Hal/Corpus">001783</idno><idno type="wicri:Area/Hal/Curation">001783</idno><idno type="wicri:Area/Hal/Checkpoint">001093</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001093</idno><idno type="wicri:Area/Main/Merge">001187</idno><idno type="wicri:Area/Main/Curation">001176</idno><idno type="wicri:Area/Main/Exploration">001176</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Computing Tiny Clause Normal Forms</title><author><name sortKey="Azmy, Noran" sort="Azmy, Noran" uniqKey="Azmy N" first="Noran" last="Azmy">Noran Azmy</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-397675" status="INCOMING"><orgName>Automation of Logic</orgName><desc><address><country key="DE"></country></address></desc><listRelation><relation active="#struct-54489" type="direct"></relation><relation active="#struct-300044" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-54489" type="direct"><org type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300044" type="indirect"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName><orgName type="acronym">MPII</orgName><desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine><country key="DE"></country></address><ref type="url">http://www.mpi-inf.mpg.de/</ref></desc><listRelation><relation active="#struct-300044" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country><orgName type="university">Société Max-Planck</orgName></affiliation></author></analytic><idno type="DOI">10.1007/978-3-642-38574-2_7</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Automated reasoning systems which build on resolution or superposition typically operate on formulas in clause normal form (CNF). It is well-known that standard CNF translation of a first-order formula may result in an exponential number of clauses. In order to prevent this effect, renaming techniques have been introduced that replace subformulas by atoms over fresh predicates and introduce definitions accordingly. This paper presents generalized renaming. Given a formula and a set of subformulas to be renamed, it is suggested to use one atom to replace all instances of a generalization of a given subformula. A generalized renaming algorithm and an implementation as part of the SPASS theorem prover are described. The new renaming algorithm is faster than the previous one implemented in SPASS. Experiments on the TPTP show that generalized renaming significantly reduces the number of clauses and the average time taken to solve the problems afterward.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><orgName><li>Société Max-Planck</li></orgName></list><tree><country name="Allemagne"><noRegion><name sortKey="Azmy, Noran" sort="Azmy, Noran" uniqKey="Azmy N" first="Noran" last="Azmy">Noran Azmy</name></noRegion><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001176 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001176 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-00931893
|texte= Computing Tiny Clause Normal Forms
}}
| This area was generated with Dilib version V0.6.33. |  |